RngSig
== car:Type
==  (eq:(carcar)
==  le:(carcar)
==  plus:(carcarcar)
==  zero:car
==  minus:(carcar)
==  times:(carcarcar)
==  (one:car
==  (carcar(?car)))) 

latex

---

clarification:

RngSig{i}
== car:Type{i}
==  (eq:(carcar)
==  le:(carcar)
==  plus:(carcarcar)
==  zero:car
==  minus:(carcar)
==  times:(carcarcar)
==  (one:car
==  (carcar(car + Unit)))) 

latex

Up	rng sig object directory
Wellformedness Lemmas	rng sig wf
Definitions	, Unit